| Definitions | t  T, True, x:A  B(x), P   Q, P  Q, x:A  B(x), P Q,  x:A. B(x),  b, type List,  x:A. B(x), a < b, False, (x l), no_repeats(T;l), left + right, P  Q, increasing(f;k), E, hd(l), (e <loc e'), e  loc e' , {x:A| B(x)} , E(X), !Void(), e < e', (e < e'), case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , ES, Type, AbsInterface(A),  , Top, sys-antecedent(es;Sys), e  X, ||as||, #$n, last(L), X(e),  T, let x,y = A in B(x;y), t.1, a:A fp B(a), strong-subtype(A;B), <a, b>,  , A c B, chain-consistent(f;chain), e c e', {T}, kind(e), Knd, first(e), source(l), destination(l), es-init(es;e), SQType(T), s ~ t, Atom$n, es-first-from(es;e;l;tg), lastchange(x;e), (last change to x before e), EState(T),  , EqDecider(T), Unit, IdLnk, EOrderAxioms(E; pred?; info), kindcase(k; a.f(a); l,t.g(l;t) ), loc(e), kind(e), Msg(M),  , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), r s, constant_function(f;A;B), SWellFounded(R(x;y)), pred!(e;e'),   x,y. t(x;y), pred(e), first(e), x. t(x), ff, inr x , tt, inl x , loc(e), f(a), Id, adjacent(T;L;x;y),  , s = t,  A, L1  L2, P & Q, isrcv(e), isrcv(k), [], [car / cdr], x before y l, A B, i j < k,  , {i..j }, A List ,  x:A.B(x), l[i], S T, suptype(S; T), Outcome, x << y |
| Lemmas | chain-order-antisymmetric, increasing wf, length wf nat, select wf, length wf1, int seg wf, le wf, l before wf, adjacent-to-same-sublist2, es-le wf, chain-consistent wf, es-causl wf, es-locl wf, btrue wf, bfalse wf, es-causle wf, es-interface wf, deq wf, EOrderAxioms wf, IdLnk wf, Msg wf, unit wf, nat wf, val-axiom wf, qle wf, cless wf, bool wf, top wf, Knd wf, kindcase wf, constant function wf, loc wf, pred! wf, strongwellfounded wf, rationals wf, EState wf, sublist wf, iff wf, rev implies wf, es-isrcv-loc, guard wf, Id sq, es-le-loc, Id wf, es-loc-pred, es-locl-iff, sys-antecedent wf, es-E-interface-subtype rel, not wf, false wf, assert wf, es-is-interface wf, member wf, es-E-interface wf, subtype rel wf, event system wf, es-E wf, true wf, squash wf, es-loc wf |
